<+>  OGrp 

latex

Up	groups 1
Definitions of Statement	|g|, , *, e, ~, Mon, AbMon, Group{i}, AbGrp, OCMon, OGrp, <+>
Definitions	OGrp, t  T, x,y. t(x;y), , x:A. B(x), x f y, P & Q, OCMon, Mon, AbMon, t.2, t.1, *, , <+>, |g|, P  Q, False, P  Q, A, AntiSym(T;x,y.R(x;y)), Trans(T;x,y.E(x;y)), Refl(T;x,y.E(x;y)), Connex(T;x,y.R(x;y)), Order(T;x,y.R(x;y)), A  B, Linorder(T;x,y.R(x;y)), Cancel(T;S;op), monot(T;x,y.R(x;y);f), ~, e, Inverse(T;op;id;inv), x(s1,s2), Group{i}, AbGrp, P  Q, P  Q, S  T
Lemmas	grp inv wf, grp id wf, grp op wf, grp car wf, inverse wf, monot wf, cancel wf, grp le wf, assert wf, linorder wf, abgrp wf, comm wf, grp eq wf, eqfun p wf, monoid p wf, grp sig inc, int add grp wf, monot functionality, assert of le int, le wf, le int wf, linorder functionality wrt iff